data NatF a = ZeroF | SuccF a